A programming language in which the type of a value is validated at run-time is a dynamically typed language. A programming language in which the type of an expression is validated at compile time is a statically typed language. In statically typed languages, the input and output types of expressions typically are explicitly provided by type annotations.
Type inference refers to the ability to deduce the type of an expression at compile time. Type inference is a feature of statically typed languages including but not limited to Visual Basic, C++, ML, OCaml, Haskell, Scala, D, Clean, Opa and Go. Functional programming languages typically include the ability to infer type. Type inference makes certain programming tasks easier because type checking is still performed by the compiler even if type annotations have been omitted from the source code.
One use of type inference in programming languages is to provide the benefits of static type checking without the need for coding that repeatedly declares type information.